<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sil (InferIR.InferIR.Sil)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc %%VERSION%%"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">InferIR</a> &#x00BB; <a href="../index.html">InferIR</a> &#x00BB; Sil</nav><h1>Module <code>InferIR.Sil</code></h1><nav class="toc"><ul><li><a href="#programs-and-types">Programs and Types</a></li><li><a href="#components-of-propositions">Components of Propositions</a></li><li><a href="#compaction">Compaction</a></li><li><a href="#pretty-printing">Pretty Printing</a></li><li><a href="#functions-for-traversing-sil-data-types">Functions for traversing SIL data types</a></li><li><a href="#substitution">Substitution</a></li><li><a href="#functions-for-replacing-occurrences-of-expressions.">Functions for replacing occurrences of expressions.</a></li><li><a href="#functions-for-constructing-or-destructing-entities-in-this-module">Functions for constructing or destructing entities in this module</a></li></ul></nav></header><div class="spec module" id="module-F"><a href="#module-F" class="anchor"></a><code><span class="keyword">module</span> F = Stdlib.Format</code></div><section><header><h3 id="programs-and-types"><a href="#programs-and-types" class="anchor"></a>Programs and Types</h3></header><dl><dt class="spec type" id="type-if_kind"><a href="#type-if_kind" class="anchor"></a><code><span class="keyword">type</span> if_kind</code><code> = </code><table class="variant"><tr id="type-if_kind.Ik_bexp" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_bexp" class="anchor"></a><code>| </code><code><span class="constructor">Ik_bexp</span></code></td><td class="doc"><p>boolean expressions, and exp ? exp : exp</p></td></tr><tr id="type-if_kind.Ik_dowhile" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_dowhile" class="anchor"></a><code>| </code><code><span class="constructor">Ik_dowhile</span></code></td></tr><tr id="type-if_kind.Ik_for" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_for" class="anchor"></a><code>| </code><code><span class="constructor">Ik_for</span></code></td></tr><tr id="type-if_kind.Ik_if" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_if" class="anchor"></a><code>| </code><code><span class="constructor">Ik_if</span></code></td></tr><tr id="type-if_kind.Ik_land_lor" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_land_lor" class="anchor"></a><code>| </code><code><span class="constructor">Ik_land_lor</span></code></td><td class="doc"><p>obtained from translation of &amp;&amp; or ||</p></td></tr><tr id="type-if_kind.Ik_while" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_while" class="anchor"></a><code>| </code><code><span class="constructor">Ik_while</span></code></td></tr><tr id="type-if_kind.Ik_switch" class="anchored"><td class="def constructor"><a href="#type-if_kind.Ik_switch" class="anchor"></a><code>| </code><code><span class="constructor">Ik_switch</span></code></td></tr></table></dt><dd><p>Kind of prune instruction</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_if_kind"><a href="#val-compare_if_kind" class="anchor"></a><code><span class="keyword">val</span> compare_if_kind : <a href="index.html#type-if_kind">if_kind</a> <span>&#45;&gt;</span> <a href="index.html#type-if_kind">if_kind</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec type" id="type-instr_metadata"><a href="#type-instr_metadata" class="anchor"></a><code><span class="keyword">type</span> instr_metadata</code><code> = </code><table class="variant"><tr id="type-instr_metadata.Abstract" class="anchored"><td class="def constructor"><a href="#type-instr_metadata.Abstract" class="anchor"></a><code>| </code><code><span class="constructor">Abstract</span> <span class="keyword">of</span> <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></td><td class="doc"><p>a good place to apply abstraction, mostly used in the biabduction analysis</p></td></tr><tr id="type-instr_metadata.ExitScope" class="anchored"><td class="def constructor"><a href="#type-instr_metadata.ExitScope" class="anchor"></a><code>| </code><code><span class="constructor">ExitScope</span> <span class="keyword">of</span> <span><a href="../Var/index.html#type-t">Var.t</a> list</span> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></td><td class="doc"><p>remove temporaries and dead program variables</p></td></tr><tr id="type-instr_metadata.Nullify" class="anchored"><td class="def constructor"><a href="#type-instr_metadata.Nullify" class="anchor"></a><code>| </code><code><span class="constructor">Nullify</span> <span class="keyword">of</span> <a href="../Pvar/index.html#type-t">Pvar.t</a> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></td><td class="doc"><p>nullify stack variable</p></td></tr><tr id="type-instr_metadata.Skip" class="anchored"><td class="def constructor"><a href="#type-instr_metadata.Skip" class="anchor"></a><code>| </code><code><span class="constructor">Skip</span></code></td><td class="doc"><p>no-op</p></td></tr><tr id="type-instr_metadata.VariableLifetimeBegins" class="anchored"><td class="def constructor"><a href="#type-instr_metadata.VariableLifetimeBegins" class="anchor"></a><code>| </code><code><span class="constructor">VariableLifetimeBegins</span> <span class="keyword">of</span> <a href="../Pvar/index.html#type-t">Pvar.t</a> * <a href="../Typ/index.html#type-t">Typ.t</a> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></td><td class="doc"><p>stack variable declared</p></td></tr></table></dt></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_instr_metadata"><a href="#val-compare_instr_metadata" class="anchor"></a><code><span class="keyword">val</span> compare_instr_metadata : <a href="index.html#type-instr_metadata">instr_metadata</a> <span>&#45;&gt;</span> <a href="index.html#type-instr_metadata">instr_metadata</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec type" id="type-instr"><a href="#type-instr" class="anchor"></a><code><span class="keyword">type</span> instr</code><code> = </code><table class="variant"><tr id="type-instr.Load" class="anchored"><td class="def constructor"><a href="#type-instr.Load" class="anchor"></a><code>| </code><code><span class="constructor">Load</span> <span class="keyword">of</span> <a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Typ/index.html#type-t">Typ.t</a> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></td><td class="doc"><p>Load a value from the heap into an identifier. <code>x = *lexp:typ</code> where <code>lexp</code> is an expression denoting a heap address <code>typ</code> is the root type of <code>lexp</code>.</p></td></tr><tr id="type-instr.Store" class="anchored"><td class="def constructor"><a href="#type-instr.Store" class="anchor"></a><code>| </code><code><span class="constructor">Store</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Typ/index.html#type-t">Typ.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></td><td class="doc"><p>Store the value of an expression into the heap. <code>*lexp1:typ = exp2</code> where <code>lexp1</code> is an expression denoting a heap address <code>typ</code> is the root type of <code>lexp1</code> <code>exp2</code> is the expression whose value is stored.</p></td></tr><tr id="type-instr.Prune" class="anchored"><td class="def constructor"><a href="#type-instr.Prune" class="anchor"></a><code>| </code><code><span class="constructor">Prune</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a> * bool * <a href="index.html#type-if_kind">if_kind</a></code></td><td class="doc"><p>prune the state based on <code>exp=1</code>, the boolean indicates whether true branch</p></td></tr><tr id="type-instr.Call" class="anchored"><td class="def constructor"><a href="#type-instr.Call" class="anchor"></a><code>| </code><code><span class="constructor">Call</span> <span class="keyword">of</span> <a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Typ/index.html#type-t">Typ.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <span><span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Typ/index.html#type-t">Typ.t</a>)</span> list</span> * <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a> * <a href="../CallFlags/index.html#type-t">CallFlags.t</a></code></td><td class="doc"><p><code>Call ((ret_id, ret_typ), e_fun, arg_ts, loc, call_flags)</code> represents an instruction <code>ret_id = e_fun(arg_ts);</code></p></td></tr><tr id="type-instr.Metadata" class="anchored"><td class="def constructor"><a href="#type-instr.Metadata" class="anchor"></a><code>| </code><code><span class="constructor">Metadata</span> <span class="keyword">of</span> <a href="index.html#type-instr_metadata">instr_metadata</a></code></td><td class="doc"><p>hints about the program that are not strictly needed to understand its semantics, for instance information about its original syntactic structure</p></td></tr></table></dt><dd><p>An instruction.</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_instr"><a href="#val-compare_instr" class="anchor"></a><code><span class="keyword">val</span> compare_instr : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-equal_instr"><a href="#val-equal_instr" class="anchor"></a><code><span class="keyword">val</span> equal_instr : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-skip_instr"><a href="#val-skip_instr" class="anchor"></a><code><span class="keyword">val</span> skip_instr : <a href="index.html#type-instr">instr</a></code></dt><dt class="spec value" id="val-instr_is_auxiliary"><a href="#val-instr_is_auxiliary" class="anchor"></a><code><span class="keyword">val</span> instr_is_auxiliary : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check if an instruction is auxiliary, or if it comes from source instructions.</p></dd></dl><dl><dt class="spec type" id="type-offset"><a href="#type-offset" class="anchor"></a><code><span class="keyword">type</span> offset</code><code> = </code><table class="variant"><tr id="type-offset.Off_fld" class="anchored"><td class="def constructor"><a href="#type-offset.Off_fld" class="anchor"></a><code>| </code><code><span class="constructor">Off_fld</span> <span class="keyword">of</span> <a href="../Typ/Fieldname/index.html#type-t">Typ.Fieldname.t</a> * <a href="../Typ/index.html#type-t">Typ.t</a></code></td></tr><tr id="type-offset.Off_index" class="anchored"><td class="def constructor"><a href="#type-offset.Off_index" class="anchor"></a><code>| </code><code><span class="constructor">Off_index</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a></code></td></tr></table></dt><dd><p>Offset for an lvalue.</p></dd></dl></section><section><header><h3 id="components-of-propositions"><a href="#components-of-propositions" class="anchor"></a>Components of Propositions</h3></header><dl><dt class="spec type" id="type-atom"><a href="#type-atom" class="anchor"></a><code><span class="keyword">type</span> atom</code><code> = </code><table class="variant"><tr id="type-atom.Aeq" class="anchored"><td class="def constructor"><a href="#type-atom.Aeq" class="anchor"></a><code>| </code><code><span class="constructor">Aeq</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a></code></td><td class="doc"><p>equality</p></td></tr><tr id="type-atom.Aneq" class="anchored"><td class="def constructor"><a href="#type-atom.Aneq" class="anchor"></a><code>| </code><code><span class="constructor">Aneq</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a></code></td><td class="doc"><p>disequality</p></td></tr><tr id="type-atom.Apred" class="anchored"><td class="def constructor"><a href="#type-atom.Apred" class="anchor"></a><code>| </code><code><span class="constructor">Apred</span> <span class="keyword">of</span> <a href="../PredSymb/index.html#type-t">PredSymb.t</a> * <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></td><td class="doc"><p>predicate symbol applied to exps</p></td></tr><tr id="type-atom.Anpred" class="anchored"><td class="def constructor"><a href="#type-atom.Anpred" class="anchor"></a><code>| </code><code><span class="constructor">Anpred</span> <span class="keyword">of</span> <a href="../PredSymb/index.html#type-t">PredSymb.t</a> * <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></td><td class="doc"><p>negated predicate symbol applied to exps</p></td></tr></table></dt><dd><p>an atom is a pure atomic formula</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_atom"><a href="#val-compare_atom" class="anchor"></a><code><span class="keyword">val</span> compare_atom : <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-equal_atom"><a href="#val-equal_atom" class="anchor"></a><code><span class="keyword">val</span> equal_atom : <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-atom_has_local_addr"><a href="#val-atom_has_local_addr" class="anchor"></a><code><span class="keyword">val</span> atom_has_local_addr : <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> bool</code></dt></dl><dl><dt class="spec type" id="type-lseg_kind"><a href="#type-lseg_kind" class="anchor"></a><code><span class="keyword">type</span> lseg_kind</code><code> = </code><table class="variant"><tr id="type-lseg_kind.Lseg_NE" class="anchored"><td class="def constructor"><a href="#type-lseg_kind.Lseg_NE" class="anchor"></a><code>| </code><code><span class="constructor">Lseg_NE</span></code></td><td class="doc"><p>nonempty (possibly circular) listseg</p></td></tr><tr id="type-lseg_kind.Lseg_PE" class="anchored"><td class="def constructor"><a href="#type-lseg_kind.Lseg_PE" class="anchor"></a><code>| </code><code><span class="constructor">Lseg_PE</span></code></td><td class="doc"><p>possibly empty (possibly circular) listseg</p></td></tr></table></dt><dd><p>kind of lseg or dllseg predicates</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_lseg_kind"><a href="#val-compare_lseg_kind" class="anchor"></a><code><span class="keyword">val</span> compare_lseg_kind : <a href="index.html#type-lseg_kind">lseg_kind</a> <span>&#45;&gt;</span> <a href="index.html#type-lseg_kind">lseg_kind</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-equal_lseg_kind"><a href="#val-equal_lseg_kind" class="anchor"></a><code><span class="keyword">val</span> equal_lseg_kind : <a href="index.html#type-lseg_kind">lseg_kind</a> <span>&#45;&gt;</span> <a href="index.html#type-lseg_kind">lseg_kind</a> <span>&#45;&gt;</span> bool</code></dt></dl><dl><dt class="spec type" id="type-zero_flag"><a href="#type-zero_flag" class="anchor"></a><code><span class="keyword">type</span> zero_flag</code><code> = <span>bool option</span></code></dt><dd><p>The boolean is true when the pointer was dereferenced without testing for zero.</p></dd></dl><dl><dt class="spec type" id="type-null_case_flag"><a href="#type-null_case_flag" class="anchor"></a><code><span class="keyword">type</span> null_case_flag</code><code> = bool</code></dt><dd><p>True when the value was obtained by doing case analysis on null in a procedure call.</p></dd></dl><dl><dt class="spec type" id="type-inst"><a href="#type-inst" class="anchor"></a><code><span class="keyword">type</span> inst</code><code> = </code><table class="variant"><tr id="type-inst.Iabstraction" class="anchored"><td class="def constructor"><a href="#type-inst.Iabstraction" class="anchor"></a><code>| </code><code><span class="constructor">Iabstraction</span></code></td></tr><tr id="type-inst.Iactual_precondition" class="anchored"><td class="def constructor"><a href="#type-inst.Iactual_precondition" class="anchor"></a><code>| </code><code><span class="constructor">Iactual_precondition</span></code></td></tr><tr id="type-inst.Ialloc" class="anchored"><td class="def constructor"><a href="#type-inst.Ialloc" class="anchor"></a><code>| </code><code><span class="constructor">Ialloc</span></code></td></tr><tr id="type-inst.Iformal" class="anchored"><td class="def constructor"><a href="#type-inst.Iformal" class="anchor"></a><code>| </code><code><span class="constructor">Iformal</span> <span class="keyword">of</span> <a href="index.html#type-zero_flag">zero_flag</a> * <a href="index.html#type-null_case_flag">null_case_flag</a></code></td></tr><tr id="type-inst.Iinitial" class="anchored"><td class="def constructor"><a href="#type-inst.Iinitial" class="anchor"></a><code>| </code><code><span class="constructor">Iinitial</span></code></td></tr><tr id="type-inst.Ilookup" class="anchored"><td class="def constructor"><a href="#type-inst.Ilookup" class="anchor"></a><code>| </code><code><span class="constructor">Ilookup</span></code></td></tr><tr id="type-inst.Inone" class="anchored"><td class="def constructor"><a href="#type-inst.Inone" class="anchor"></a><code>| </code><code><span class="constructor">Inone</span></code></td></tr><tr id="type-inst.Inullify" class="anchored"><td class="def constructor"><a href="#type-inst.Inullify" class="anchor"></a><code>| </code><code><span class="constructor">Inullify</span></code></td></tr><tr id="type-inst.Irearrange" class="anchored"><td class="def constructor"><a href="#type-inst.Irearrange" class="anchor"></a><code>| </code><code><span class="constructor">Irearrange</span> <span class="keyword">of</span> <a href="index.html#type-zero_flag">zero_flag</a> * <a href="index.html#type-null_case_flag">null_case_flag</a> * int * <a href="../PredSymb/index.html#type-path_pos">PredSymb.path_pos</a></code></td></tr><tr id="type-inst.Itaint" class="anchored"><td class="def constructor"><a href="#type-inst.Itaint" class="anchor"></a><code>| </code><code><span class="constructor">Itaint</span></code></td></tr><tr id="type-inst.Iupdate" class="anchored"><td class="def constructor"><a href="#type-inst.Iupdate" class="anchor"></a><code>| </code><code><span class="constructor">Iupdate</span> <span class="keyword">of</span> <a href="index.html#type-zero_flag">zero_flag</a> * <a href="index.html#type-null_case_flag">null_case_flag</a> * int * <a href="../PredSymb/index.html#type-path_pos">PredSymb.path_pos</a></code></td></tr><tr id="type-inst.Ireturn_from_call" class="anchored"><td class="def constructor"><a href="#type-inst.Ireturn_from_call" class="anchor"></a><code>| </code><code><span class="constructor">Ireturn_from_call</span> <span class="keyword">of</span> int</code></td></tr></table></dt><dd><p>instrumentation of heap values</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_inst"><a href="#val-compare_inst" class="anchor"></a><code><span class="keyword">val</span> compare_inst : <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-equal_inst"><a href="#val-equal_inst" class="anchor"></a><code><span class="keyword">val</span> equal_inst : <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-inst_actual_precondition"><a href="#val-inst_actual_precondition" class="anchor"></a><code><span class="keyword">val</span> inst_actual_precondition : <a href="index.html#type-inst">inst</a></code></dt><dt class="spec value" id="val-inst_formal"><a href="#val-inst_formal" class="anchor"></a><code><span class="keyword">val</span> inst_formal : <a href="index.html#type-inst">inst</a></code></dt><dt class="spec value" id="val-inst_initial"><a href="#val-inst_initial" class="anchor"></a><code><span class="keyword">val</span> inst_initial : <a href="index.html#type-inst">inst</a></code></dt><dd><p>for formal parameters and heap values at the beginning of the function</p></dd></dl><dl><dt class="spec value" id="val-inst_lookup"><a href="#val-inst_lookup" class="anchor"></a><code><span class="keyword">val</span> inst_lookup : <a href="index.html#type-inst">inst</a></code></dt><dd><p>for initial values</p></dd></dl><dl><dt class="spec value" id="val-inst_none"><a href="#val-inst_none" class="anchor"></a><code><span class="keyword">val</span> inst_none : <a href="index.html#type-inst">inst</a></code></dt><dt class="spec value" id="val-inst_nullify"><a href="#val-inst_nullify" class="anchor"></a><code><span class="keyword">val</span> inst_nullify : <a href="index.html#type-inst">inst</a></code></dt><dt class="spec value" id="val-inst_rearrange"><a href="#val-inst_rearrange" class="anchor"></a><code><span class="keyword">val</span> inst_rearrange : bool <span>&#45;&gt;</span> <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a> <span>&#45;&gt;</span> <a href="../PredSymb/index.html#type-path_pos">PredSymb.path_pos</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dd><p>the boolean indicates whether the pointer is known nonzero</p></dd></dl><dl><dt class="spec value" id="val-inst_update"><a href="#val-inst_update" class="anchor"></a><code><span class="keyword">val</span> inst_update : <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a> <span>&#45;&gt;</span> <a href="../PredSymb/index.html#type-path_pos">PredSymb.path_pos</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dt class="spec value" id="val-inst_set_null_case_flag"><a href="#val-inst_set_null_case_flag" class="anchor"></a><code><span class="keyword">val</span> inst_set_null_case_flag : <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dd><p>Set the null case flag of the inst.</p></dd></dl><dl><dt class="spec value" id="val-inst_new_loc"><a href="#val-inst_new_loc" class="anchor"></a><code><span class="keyword">val</span> inst_new_loc : <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dd><p>update the location of the instrumentation</p></dd></dl><dl><dt class="spec value" id="val-update_inst"><a href="#val-update_inst" class="anchor"></a><code><span class="keyword">val</span> update_inst : <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dd><p>Update <code>inst_old</code> to <code>inst_new</code> preserving the zero flag</p></dd></dl><dl><dt class="spec exception" id="exception-JoinFail"><a href="#exception-JoinFail" class="anchor"></a><code><span class="keyword">exception</span> </code><code><span class="exception">JoinFail</span></code></dt></dl><dl><dt class="spec value" id="val-inst_partial_join"><a href="#val-inst_partial_join" class="anchor"></a><code><span class="keyword">val</span> inst_partial_join : <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dd><p>join of instrumentations, can raise JoinFail</p></dd></dl><dl><dt class="spec value" id="val-inst_partial_meet"><a href="#val-inst_partial_meet" class="anchor"></a><code><span class="keyword">val</span> inst_partial_meet : <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a></code></dt><dd><p>meet of instrumentations</p></dd></dl><dl><dt class="spec type" id="type-strexp0"><a href="#type-strexp0" class="anchor"></a><code><span class="keyword">type</span> <span>'inst strexp0</span></code><code> = </code><table class="variant"><tr id="type-strexp0.Eexp" class="anchored"><td class="def constructor"><a href="#type-strexp0.Eexp" class="anchor"></a><code>| </code><code><span class="constructor">Eexp</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <span class="type-var">'inst</span></code></td><td class="doc"><p>Base case: expression with instrumentation</p></td></tr><tr id="type-strexp0.Estruct" class="anchored"><td class="def constructor"><a href="#type-strexp0.Estruct" class="anchor"></a><code>| </code><code><span class="constructor">Estruct</span> <span class="keyword">of</span> <span><span>(<a href="../Typ/Fieldname/index.html#type-t">Typ.Fieldname.t</a> * <span><span class="type-var">'inst</span> <a href="index.html#type-strexp0">strexp0</a></span>)</span> list</span> * <span class="type-var">'inst</span></code></td><td class="doc"><p>C structure</p></td></tr><tr id="type-strexp0.Earray" class="anchored"><td class="def constructor"><a href="#type-strexp0.Earray" class="anchor"></a><code>| </code><code><span class="constructor">Earray</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <span><span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <span><span class="type-var">'inst</span> <a href="index.html#type-strexp0">strexp0</a></span>)</span> list</span> * <span class="type-var">'inst</span></code></td><td class="doc"><p>Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array in a strexp, then the index is less than the length of the array. For instance, x |-&gt;<code>10 | e1: v1</code> implies that e1 &lt;= 9. Second, if two indices appear in an array, they should be different. For instance, x |-&gt;<code>10 | e1: v1, e2: v2</code> implies that e1 != e2.</p></td></tr></table></dt><dd><p>structured expressions represent a value of structured type, such as an array or a struct.</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_strexp0"><a href="#val-compare_strexp0" class="anchor"></a><code><span class="keyword">val</span> compare_strexp0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-strexp0">strexp0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-strexp0">strexp0</a></span> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec type" id="type-strexp"><a href="#type-strexp" class="anchor"></a><code><span class="keyword">type</span> strexp</code><code> = <span><a href="index.html#type-inst">inst</a> <a href="index.html#type-strexp0">strexp0</a></span></code></dt></dl><dl><dt class="spec value" id="val-compare_strexp"><a href="#val-compare_strexp" class="anchor"></a><code><span class="keyword">val</span> compare_strexp : <span>?&#8288;inst:bool</span> <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Comparison function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).</p></dd></dl><dl><dt class="spec value" id="val-equal_strexp"><a href="#val-equal_strexp" class="anchor"></a><code><span class="keyword">val</span> equal_strexp : <span>?&#8288;inst:bool</span> <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Equality function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).</p></dd></dl><dl><dt class="spec type" id="type-hpred0"><a href="#type-hpred0" class="anchor"></a><code><span class="keyword">type</span> <span>'inst hpred0</span></code><code> = </code><table class="variant"><tr id="type-hpred0.Hpointsto" class="anchored"><td class="def constructor"><a href="#type-hpred0.Hpointsto" class="anchor"></a><code>| </code><code><span class="constructor">Hpointsto</span> <span class="keyword">of</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <span><span class="type-var">'inst</span> <a href="index.html#type-strexp0">strexp0</a></span> * <a href="../Exp/index.html#type-t">Exp.t</a></code></td><td class="doc"><p>represents <code>exp|-&gt;strexp:typexp</code> where <code>typexp</code> is an expression representing a type, e.h. <code>sizeof(t)</code>.</p></td></tr><tr id="type-hpred0.Hlseg" class="anchored"><td class="def constructor"><a href="#type-hpred0.Hlseg" class="anchor"></a><code>| </code><code><span class="constructor">Hlseg</span> <span class="keyword">of</span> <a href="index.html#type-lseg_kind">lseg_kind</a> * <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> * <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></td><td class="doc"><p>higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last <code>exp list</code> parameter is used to denote the shared links by all the nodes in the list.</p></td></tr><tr id="type-hpred0.Hdllseg" class="anchored"><td class="def constructor"><a href="#type-hpred0.Hdllseg" class="anchor"></a><code>| </code><code><span class="constructor">Hdllseg</span> <span class="keyword">of</span> <a href="index.html#type-lseg_kind">lseg_kind</a> * <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> * <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></td><td class="doc"><p>higher-order predicate for doubly-linked lists. Parameter for the higher-order singly-linked list predicate. Means &quot;lambda (root,next,svars). Exists evars. body&quot;. Assume that root, next, svars, evars are disjoint sets of primed identifiers, and include all the free primed identifiers in body. body should not contain any non - primed identifiers or program variables (i.e. pvars).</p></td></tr></table></dt><dd><p>an atomic heap predicate</p></dd></dl><dl><dt class="spec type" id="type-hpara0"><a href="#type-hpara0" class="anchor"></a><code><span class="keyword">and</span> <span>'inst hpara0</span></code><code> = </code><code>{</code><table class="record"><tr id="type-hpara0.root" class="anchored"><td class="def field"><a href="#type-hpara0.root" class="anchor"></a><code>root : <a href="../Ident/index.html#type-t">Ident.t</a>;</code></td></tr><tr id="type-hpara0.next" class="anchored"><td class="def field"><a href="#type-hpara0.next" class="anchor"></a><code>next : <a href="../Ident/index.html#type-t">Ident.t</a>;</code></td></tr><tr id="type-hpara0.svars" class="anchored"><td class="def field"><a href="#type-hpara0.svars" class="anchor"></a><code>svars : <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span>;</code></td></tr><tr id="type-hpara0.evars" class="anchored"><td class="def field"><a href="#type-hpara0.evars" class="anchor"></a><code>evars : <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span>;</code></td></tr><tr id="type-hpara0.body" class="anchored"><td class="def field"><a href="#type-hpara0.body" class="anchor"></a><code>body : <span><span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> list</span>;</code></td></tr></table><code>}</code></dt><dt class="spec type" id="type-hpara_dll0"><a href="#type-hpara_dll0" class="anchor"></a><code><span class="keyword">and</span> <span>'inst hpara_dll0</span></code><code> = </code><code>{</code><table class="record"><tr id="type-hpara_dll0.cell" class="anchored"><td class="def field"><a href="#type-hpara_dll0.cell" class="anchor"></a><code>cell : <a href="../Ident/index.html#type-t">Ident.t</a>;</code></td><td class="doc"><p>address cell</p></td></tr><tr id="type-hpara_dll0.blink" class="anchored"><td class="def field"><a href="#type-hpara_dll0.blink" class="anchor"></a><code>blink : <a href="../Ident/index.html#type-t">Ident.t</a>;</code></td><td class="doc"><p>backward link</p></td></tr><tr id="type-hpara_dll0.flink" class="anchored"><td class="def field"><a href="#type-hpara_dll0.flink" class="anchor"></a><code>flink : <a href="../Ident/index.html#type-t">Ident.t</a>;</code></td><td class="doc"><p>forward link</p></td></tr><tr id="type-hpara_dll0.svars_dll" class="anchored"><td class="def field"><a href="#type-hpara_dll0.svars_dll" class="anchor"></a><code>svars_dll : <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span>;</code></td></tr><tr id="type-hpara_dll0.evars_dll" class="anchored"><td class="def field"><a href="#type-hpara_dll0.evars_dll" class="anchor"></a><code>evars_dll : <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span>;</code></td></tr><tr id="type-hpara_dll0.body_dll" class="anchored"><td class="def field"><a href="#type-hpara_dll0.body_dll" class="anchor"></a><code>body_dll : <span><span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> list</span>;</code></td></tr></table><code>}</code></dt><dd><p>parameter for the higher-order doubly-linked list predicates. Assume that all the free identifiers in body_dll should belong to cell, blink, flink, svars_dll, evars_dll.</p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_hpred0"><a href="#val-compare_hpred0" class="anchor"></a><code><span class="keyword">val</span> compare_hpred0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpara0"><a href="#val-compare_hpara0" class="anchor"></a><code><span class="keyword">val</span> compare_hpara0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpara_dll0"><a href="#val-compare_hpara_dll0" class="anchor"></a><code><span class="keyword">val</span> compare_hpara_dll0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpred0"><a href="#val-compare_hpred0" class="anchor"></a><code><span class="keyword">val</span> compare_hpred0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpara0"><a href="#val-compare_hpara0" class="anchor"></a><code><span class="keyword">val</span> compare_hpara0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpara_dll0"><a href="#val-compare_hpara_dll0" class="anchor"></a><code><span class="keyword">val</span> compare_hpara_dll0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpred0"><a href="#val-compare_hpred0" class="anchor"></a><code><span class="keyword">val</span> compare_hpred0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpred0">hpred0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpara0"><a href="#val-compare_hpara0" class="anchor"></a><code><span class="keyword">val</span> compare_hpara0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara0">hpara0</a></span> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-compare_hpara_dll0"><a href="#val-compare_hpara_dll0" class="anchor"></a><code><span class="keyword">val</span> compare_hpara_dll0 : <span>(<span class="type-var">'inst</span> <span>&#45;&gt;</span> <span class="type-var">'inst</span> <span>&#45;&gt;</span> int)</span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> <span>&#45;&gt;</span> <span><span class="type-var">'inst</span> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec type" id="type-hpred"><a href="#type-hpred" class="anchor"></a><code><span class="keyword">type</span> hpred</code><code> = <span><a href="index.html#type-inst">inst</a> <a href="index.html#type-hpred0">hpred0</a></span></code></dt><dt class="spec type" id="type-hpara"><a href="#type-hpara" class="anchor"></a><code><span class="keyword">type</span> hpara</code><code> = <span><a href="index.html#type-inst">inst</a> <a href="index.html#type-hpara0">hpara0</a></span></code></dt><dt class="spec type" id="type-hpara_dll"><a href="#type-hpara_dll" class="anchor"></a><code><span class="keyword">type</span> hpara_dll</code><code> = <span><a href="index.html#type-inst">inst</a> <a href="index.html#type-hpara_dll0">hpara_dll0</a></span></code></dt></dl><dl><dt class="spec value" id="val-compare_hpred"><a href="#val-compare_hpred" class="anchor"></a><code><span class="keyword">val</span> compare_hpred : <span>?&#8288;inst:bool</span> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Comparison function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).</p></dd></dl><dl><dt class="spec value" id="val-equal_hpred"><a href="#val-equal_hpred" class="anchor"></a><code><span class="keyword">val</span> equal_hpred : <span>?&#8288;inst:bool</span> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Equality function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).</p></dd></dl><dl><dt class="spec module" id="module-HpredSet"><a href="#module-HpredSet" class="anchor"></a><code><span class="keyword">module</span> HpredSet : <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Caml.Set.S <span class="keyword">with</span> <span class="keyword">type</span> <a href="index.html#module-HpredSet">HpredSet</a>.elt = <a href="index.html#type-hpred">hpred</a></code></dt><dd><p>Sets of heap predicates</p></dd></dl></section><section><header><h3 id="compaction"><a href="#compaction" class="anchor"></a>Compaction</h3></header><dl><dt class="spec type" id="type-sharing_env"><a href="#type-sharing_env" class="anchor"></a><code><span class="keyword">type</span> sharing_env</code></dt></dl><dl><dt class="spec value" id="val-create_sharing_env"><a href="#val-create_sharing_env" class="anchor"></a><code><span class="keyword">val</span> create_sharing_env : unit <span>&#45;&gt;</span> <a href="index.html#type-sharing_env">sharing_env</a></code></dt><dd><p>Create a sharing env to store canonical representations</p></dd></dl><dl><dt class="spec value" id="val-hpred_compact"><a href="#val-hpred_compact" class="anchor"></a><code><span class="keyword">val</span> hpred_compact : <a href="index.html#type-sharing_env">sharing_env</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a></code></dt><dd><p>Return a compact representation of the exp</p></dd></dl><dl><dt class="spec value" id="val-is_objc_object"><a href="#val-is_objc_object" class="anchor"></a><code><span class="keyword">val</span> is_objc_object : <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> bool</code></dt><dd><h3 id="comparision-and-inspection-functions"><a href="#comparision-and-inspection-functions" class="anchor"></a>Comparision And Inspection Functions</h3></dd></dl><dl><dt class="spec value" id="val-is_static_local_name"><a href="#val-is_static_local_name" class="anchor"></a><code><span class="keyword">val</span> is_static_local_name : string <span>&#45;&gt;</span> <a href="../Pvar/index.html#type-t">Pvar.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check if a pvar is a local static in objc</p></dd></dl><dl><dt class="spec value" id="val-is_block_pvar"><a href="#val-is_block_pvar" class="anchor"></a><code><span class="keyword">val</span> is_block_pvar : <a href="../Pvar/index.html#type-t">Pvar.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check if a pvar is a local pointing to a block in objc</p></dd></dl><dl><dt class="spec value" id="val-add_with_block_parameters_flag"><a href="#val-add_with_block_parameters_flag" class="anchor"></a><code><span class="keyword">val</span> add_with_block_parameters_flag : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> <a href="index.html#type-instr">instr</a></code></dt><dd><p>Adds a with_blocks_parameters flag to a method call, when the arguments contain an Objective-C block, and the method is an Objective-C method (to be extended to other methods)</p></dd></dl></section><section><header><h3 id="pretty-printing"><a href="#pretty-printing" class="anchor"></a>Pretty Printing</h3></header><dl><dt class="spec value" id="val-color_wrapper"><a href="#val-color_wrapper" class="anchor"></a><code><span class="keyword">val</span> color_wrapper : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span>f:<span>(<a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Wraps a printing function with an updated printenv when using diff printing</p></dd></dl><dl><dt class="spec value" id="val-pp_exp_printenv"><a href="#val-pp_exp_printenv" class="anchor"></a><code><span class="keyword">val</span> pp_exp_printenv : <span>?&#8288;print_types:bool</span> <span>&#45;&gt;</span> <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print an expression.</p></dd></dl><dl><dt class="spec value" id="val-d_exp"><a href="#val-d_exp" class="anchor"></a><code><span class="keyword">val</span> d_exp : <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>dump an expression.</p></dd></dl><dl><dt class="spec value" id="val-pp_texp"><a href="#val-pp_texp" class="anchor"></a><code><span class="keyword">val</span> pp_texp : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a type.</p></dd></dl><dl><dt class="spec value" id="val-pp_texp_full"><a href="#val-pp_texp_full" class="anchor"></a><code><span class="keyword">val</span> pp_texp_full : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a type with all the details.</p></dd></dl><dl><dt class="spec value" id="val-d_texp_full"><a href="#val-d_texp_full" class="anchor"></a><code><span class="keyword">val</span> d_texp_full : <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump a type expression with all the details.</p></dd></dl><dl><dt class="spec value" id="val-d_exp_list"><a href="#val-d_exp_list" class="anchor"></a><code><span class="keyword">val</span> d_exp_list : <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump a list of expressions.</p></dd></dl><dl><dt class="spec value" id="val-pp_offset"><a href="#val-pp_offset" class="anchor"></a><code><span class="keyword">val</span> pp_offset : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-offset">offset</a> <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-d_offset_list"><a href="#val-d_offset_list" class="anchor"></a><code><span class="keyword">val</span> d_offset_list : <span><a href="index.html#type-offset">offset</a> list</span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump a list of offsets</p></dd></dl><dl><dt class="spec value" id="val-location_of_instr"><a href="#val-location_of_instr" class="anchor"></a><code><span class="keyword">val</span> location_of_instr : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> <a href="../../../InferBase/InferBase/Location/index.html#type-t">InferBase.Location.t</a></code></dt><dd><p>Get the location of the instruction</p></dd></dl><dl><dt class="spec value" id="val-exps_of_instr"><a href="#val-exps_of_instr" class="anchor"></a><code><span class="keyword">val</span> exps_of_instr : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></dt><dd><p>get the expressions occurring in the instruction</p></dd></dl><dl><dt class="spec value" id="val-if_kind_to_string"><a href="#val-if_kind_to_string" class="anchor"></a><code><span class="keyword">val</span> if_kind_to_string : <a href="index.html#type-if_kind">if_kind</a> <span>&#45;&gt;</span> string</code></dt><dd><p>Pretty print an if_kind</p></dd></dl><dl><dt class="spec value" id="val-pp_instr_metadata"><a href="#val-pp_instr_metadata" class="anchor"></a><code><span class="keyword">val</span> pp_instr_metadata : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-instr_metadata">instr_metadata</a> <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-pp_instr"><a href="#val-pp_instr" class="anchor"></a><code><span class="keyword">val</span> pp_instr : <span>print_types:bool</span> <span>&#45;&gt;</span> <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print an instruction.</p></dd></dl><dl><dt class="spec value" id="val-d_instr"><a href="#val-d_instr" class="anchor"></a><code><span class="keyword">val</span> d_instr : <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump an instruction.</p></dd></dl><dl><dt class="spec value" id="val-pp_atom"><a href="#val-pp_atom" class="anchor"></a><code><span class="keyword">val</span> pp_atom : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print an atom.</p></dd></dl><dl><dt class="spec value" id="val-d_atom"><a href="#val-d_atom" class="anchor"></a><code><span class="keyword">val</span> d_atom : <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump an atom.</p></dd></dl><dl><dt class="spec value" id="val-pp_inst"><a href="#val-pp_inst" class="anchor"></a><code><span class="keyword">val</span> pp_inst : <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>pretty-print an inst</p></dd></dl><dl><dt class="spec value" id="val-pp_sexp"><a href="#val-pp_sexp" class="anchor"></a><code><span class="keyword">val</span> pp_sexp : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a strexp.</p></dd></dl><dl><dt class="spec value" id="val-d_sexp"><a href="#val-d_sexp" class="anchor"></a><code><span class="keyword">val</span> d_sexp : <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump a strexp.</p></dd></dl><dl><dt class="spec value" id="val-pp_hpred"><a href="#val-pp_hpred" class="anchor"></a><code><span class="keyword">val</span> pp_hpred : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a hpred.</p></dd></dl><dl><dt class="spec value" id="val-d_hpred"><a href="#val-d_hpred" class="anchor"></a><code><span class="keyword">val</span> d_hpred : <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Dump a hpred.</p></dd></dl><dl><dt class="spec value" id="val-pp_hpara"><a href="#val-pp_hpara" class="anchor"></a><code><span class="keyword">val</span> pp_hpara : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-hpara">hpara</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a hpara.</p></dd></dl><dl><dt class="spec value" id="val-pp_hpara_dll"><a href="#val-pp_hpara_dll" class="anchor"></a><code><span class="keyword">val</span> pp_hpara_dll : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-hpara_dll">hpara_dll</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a hpara_dll.</p></dd></dl><dl><dt class="spec module" id="module-Predicates"><a href="#module-Predicates" class="anchor"></a><code><span class="keyword">module</span> <a href="Predicates/index.html">Predicates</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Module Predicates records the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator.</p></dd></dl><dl><dt class="spec value" id="val-pp_hpred_env"><a href="#val-pp_hpred_env" class="anchor"></a><code><span class="keyword">val</span> pp_hpred_env : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span>&#45;&gt;</span> <span><a href="Predicates/index.html#type-env">Predicates.env</a> option</span> <span>&#45;&gt;</span> <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a hpred with optional predicate env</p></dd></dl></section><section><header><h3 id="functions-for-traversing-sil-data-types"><a href="#functions-for-traversing-sil-data-types" class="anchor"></a>Functions for traversing SIL data types</h3></header><dl><dt class="spec value" id="val-strexp_expmap"><a href="#val-strexp_expmap" class="anchor"></a><code><span class="keyword">val</span> strexp_expmap : <span>(<span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="index.html#type-inst">inst</a> option</span>)</span> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="index.html#type-inst">inst</a> option</span>)</span> <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a> <span>&#45;&gt;</span> <a href="index.html#type-strexp">strexp</a></code></dt><dd><p>Change exps in strexp using <code>f</code>. WARNING: the result might not be normalized.</p></dd></dl><dl><dt class="spec value" id="val-hpred_expmap"><a href="#val-hpred_expmap" class="anchor"></a><code><span class="keyword">val</span> hpred_expmap : <span>(<span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="index.html#type-inst">inst</a> option</span>)</span> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="index.html#type-inst">inst</a> option</span>)</span> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a></code></dt><dd><p>Change exps in hpred by <code>f</code>. WARNING: the result might not be normalized.</p></dd></dl><dl><dt class="spec value" id="val-hpred_instmap"><a href="#val-hpred_instmap" class="anchor"></a><code><span class="keyword">val</span> hpred_instmap : <span>(<a href="index.html#type-inst">inst</a> <span>&#45;&gt;</span> <a href="index.html#type-inst">inst</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a></code></dt><dd><p>Change instrumentations in hpred using <code>f</code>.</p></dd></dl><dl><dt class="spec value" id="val-hpred_list_expmap"><a href="#val-hpred_list_expmap" class="anchor"></a><code><span class="keyword">val</span> hpred_list_expmap : <span>(<span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="index.html#type-inst">inst</a> option</span>)</span> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> * <span><a href="index.html#type-inst">inst</a> option</span>)</span> <span>&#45;&gt;</span> <span><a href="index.html#type-hpred">hpred</a> list</span> <span>&#45;&gt;</span> <span><a href="index.html#type-hpred">hpred</a> list</span></code></dt><dd><p>Change exps in hpred list by <code>f</code>. WARNING: the result might not be normalized.</p></dd></dl><dl><dt class="spec value" id="val-atom_expmap"><a href="#val-atom_expmap" class="anchor"></a><code><span class="keyword">val</span> atom_expmap : <span>(<a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a></code></dt><dd><p>Change exps in atom by <code>f</code>. WARNING: the result might not be normalized.</p></dd></dl><dl><dt class="spec value" id="val-hpred_list_get_lexps"><a href="#val-hpred_list_get_lexps" class="anchor"></a><code><span class="keyword">val</span> hpred_list_get_lexps : <span>(<a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <span><a href="index.html#type-hpred">hpred</a> list</span> <span>&#45;&gt;</span> <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></dt><dt class="spec value" id="val-hpred_entries"><a href="#val-hpred_entries" class="anchor"></a><code><span class="keyword">val</span> hpred_entries : <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></dt><dt class="spec value" id="val-atom_free_vars"><a href="#val-atom_free_vars" class="anchor"></a><code><span class="keyword">val</span> atom_free_vars : <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dt class="spec value" id="val-atom_gen_free_vars"><a href="#val-atom_gen_free_vars" class="anchor"></a><code><span class="keyword">val</span> atom_gen_free_vars : <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <span><span>(unit, <a href="../Ident/index.html#type-t">Ident.t</a>)</span> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.Generator.t</span></code></dt><dt class="spec value" id="val-hpred_free_vars"><a href="#val-hpred_free_vars" class="anchor"></a><code><span class="keyword">val</span> hpred_free_vars : <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dt class="spec value" id="val-hpred_gen_free_vars"><a href="#val-hpred_gen_free_vars" class="anchor"></a><code><span class="keyword">val</span> hpred_gen_free_vars : <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <span><span>(unit, <a href="../Ident/index.html#type-t">Ident.t</a>)</span> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.Generator.t</span></code></dt><dt class="spec value" id="val-hpara_shallow_free_vars"><a href="#val-hpara_shallow_free_vars" class="anchor"></a><code><span class="keyword">val</span> hpara_shallow_free_vars : <a href="index.html#type-hpara">hpara</a> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dt class="spec value" id="val-hpara_dll_shallow_free_vars"><a href="#val-hpara_dll_shallow_free_vars" class="anchor"></a><code><span class="keyword">val</span> hpara_dll_shallow_free_vars : <a href="index.html#type-hpara_dll">hpara_dll</a> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dd><p>Variables in hpara_dll, excluding bound vars in the body</p></dd></dl></section><section><header><h3 id="substitution"><a href="#substitution" class="anchor"></a>Substitution</h3></header><dl><dt class="spec type" id="type-subst"><a href="#type-subst" class="anchor"></a><code><span class="keyword">type</span> subst</code><code> = <span class="keyword">private</span> <span><span>(<a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span></code></dt></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_subst"><a href="#val-compare_subst" class="anchor"></a><code><span class="keyword">val</span> compare_subst : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-equal_subst"><a href="#val-equal_subst" class="anchor"></a><code><span class="keyword">val</span> equal_subst : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Equality for substitutions.</p></dd></dl><dl><dt class="spec value" id="val-subst_of_list"><a href="#val-subst_of_list" class="anchor"></a><code><span class="keyword">val</span> subst_of_list : <span><span>(<a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p>Create a substitution from a list of pairs. For all (id1, e1), (id2, e2) in the input list, if id1 = id2, then e1 = e2.</p></dd></dl><dl><dt class="spec value" id="val-subst_of_list_duplicates"><a href="#val-subst_of_list_duplicates" class="anchor"></a><code><span class="keyword">val</span> subst_of_list_duplicates : <span><span>(<a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p>like subst_of_list, but allow duplicate ids and only keep the first occurrence</p></dd></dl><dl><dt class="spec value" id="val-sub_to_list"><a href="#val-sub_to_list" class="anchor"></a><code><span class="keyword">val</span> sub_to_list : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <span><span>(<a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span></code></dt><dd><p>Convert a subst to a list of pairs.</p></dd></dl><dl><dt class="spec value" id="val-sub_empty"><a href="#val-sub_empty" class="anchor"></a><code><span class="keyword">val</span> sub_empty : <a href="index.html#type-subst">subst</a></code></dt><dd><p>The empty substitution.</p></dd></dl><dl><dt class="spec value" id="val-is_sub_empty"><a href="#val-is_sub_empty" class="anchor"></a><code><span class="keyword">val</span> is_sub_empty : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-sub_join"><a href="#val-sub_join" class="anchor"></a><code><span class="keyword">val</span> sub_join : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p>Compute the common id-exp part of two inputs <code>subst1</code> and <code>subst2</code>. The first component of the output is this common part. The second and third components are the remainder of <code>subst1</code> and <code>subst2</code>, respectively.</p></dd></dl><dl><dt class="spec value" id="val-sub_symmetric_difference"><a href="#val-sub_symmetric_difference" class="anchor"></a><code><span class="keyword">val</span> sub_symmetric_difference : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> * <a href="index.html#type-subst">subst</a> * <a href="index.html#type-subst">subst</a></code></dt><dd><p>Compute the common id-exp part of two inputs <code>subst1</code> and <code>subst2</code>. The first component of the output is this common part. The second and third components are the remainder of <code>subst1</code> and <code>subst2</code>, respectively.</p></dd></dl><dl><dt class="spec value" id="val-sub_find"><a href="#val-sub_find" class="anchor"></a><code><span class="keyword">val</span> sub_find : <span>(<a href="../Ident/index.html#type-t">Ident.t</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a></code></dt><dd><p><code>sub_find filter sub</code> returns the expression associated to the first identifier that satisfies <code>filter</code>. Raise <code>Not_found</code> if there isn't one.</p></dd></dl><dl><dt class="spec value" id="val-sub_filter"><a href="#val-sub_filter" class="anchor"></a><code><span class="keyword">val</span> sub_filter : <span>(<a href="../Ident/index.html#type-t">Ident.t</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p><code>sub_filter filter sub</code> restricts the domain of <code>sub</code> to the identifiers satisfying <code>filter</code>.</p></dd></dl><dl><dt class="spec value" id="val-sub_filter_pair"><a href="#val-sub_filter_pair" class="anchor"></a><code><span class="keyword">val</span> sub_filter_pair : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <span>f:<span>(<span>(<a href="../Ident/index.html#type-t">Ident.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> <span>&#45;&gt;</span> bool)</span></span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p><code>sub_filter_exp filter sub</code> restricts the domain of <code>sub</code> to the identifiers satisfying <code>filter(id, sub(id))</code>.</p></dd></dl><dl><dt class="spec value" id="val-sub_range_partition"><a href="#val-sub_range_partition" class="anchor"></a><code><span class="keyword">val</span> sub_range_partition : <span>(<a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> * <a href="index.html#type-subst">subst</a></code></dt><dd><p><code>sub_range_partition filter sub</code> partitions <code>sub</code> according to whether range expressions satisfy <code>filter</code>.</p></dd></dl><dl><dt class="spec value" id="val-sub_domain_partition"><a href="#val-sub_domain_partition" class="anchor"></a><code><span class="keyword">val</span> sub_domain_partition : <span>(<a href="../Ident/index.html#type-t">Ident.t</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> * <a href="index.html#type-subst">subst</a></code></dt><dd><p><code>sub_domain_partition filter sub</code> partitions <code>sub</code> according to whether domain identifiers satisfy <code>filter</code>.</p></dd></dl><dl><dt class="spec value" id="val-sub_domain"><a href="#val-sub_domain" class="anchor"></a><code><span class="keyword">val</span> sub_domain : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span></code></dt><dd><p>Return the list of identifiers in the domain of the substitution.</p></dd></dl><dl><dt class="spec value" id="val-sub_range"><a href="#val-sub_range" class="anchor"></a><code><span class="keyword">val</span> sub_range : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span></code></dt><dd><p>Return the list of expressions in the range of the substitution.</p></dd></dl><dl><dt class="spec value" id="val-sub_range_map"><a href="#val-sub_range_map" class="anchor"></a><code><span class="keyword">val</span> sub_range_map : <span>(<a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p><code>sub_range_map f sub</code> applies <code>f</code> to the expressions in the range of <code>sub</code>.</p></dd></dl><dl><dt class="spec value" id="val-sub_map"><a href="#val-sub_map" class="anchor"></a><code><span class="keyword">val</span> sub_map : <span>(<a href="../Ident/index.html#type-t">Ident.t</a> <span>&#45;&gt;</span> <a href="../Ident/index.html#type-t">Ident.t</a>)</span> <span>&#45;&gt;</span> <span>(<a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-subst">subst</a></code></dt><dd><p><code>sub_map f g sub</code> applies the renaming <code>f</code> to identifiers in the domain of <code>sub</code> and the substitution <code>g</code> to the expressions in the range of <code>sub</code>.</p></dd></dl><dl><dt class="spec value" id="val-extend_sub"><a href="#val-extend_sub" class="anchor"></a><code><span class="keyword">val</span> extend_sub : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="../Ident/index.html#type-t">Ident.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-subst">subst</a> option</span></code></dt><dd><p>Extend substitution and return <code>None</code> if not possible.</p></dd></dl><dl><dt class="spec value" id="val-subst_free_vars"><a href="#val-subst_free_vars" class="anchor"></a><code><span class="keyword">val</span> subst_free_vars : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</span></code></dt><dt class="spec value" id="val-subst_gen_free_vars"><a href="#val-subst_gen_free_vars" class="anchor"></a><code><span class="keyword">val</span> subst_gen_free_vars : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <span><span>(unit, <a href="../Ident/index.html#type-t">Ident.t</a>)</span> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.Generator.t</span></code></dt></dl><aside><p>substitution functions WARNING: these functions do not ensure that the results are normalized.</p></aside><dl><dt class="spec value" id="val-exp_sub"><a href="#val-exp_sub" class="anchor"></a><code><span class="keyword">val</span> exp_sub : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a></code></dt><dt class="spec value" id="val-atom_sub"><a href="#val-atom_sub" class="anchor"></a><code><span class="keyword">val</span> atom_sub : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a></code></dt><dt class="spec value" id="val-instr_sub"><a href="#val-instr_sub" class="anchor"></a><code><span class="keyword">val</span> instr_sub : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-instr">instr</a> <span>&#45;&gt;</span> <a href="index.html#type-instr">instr</a></code></dt><dd><p>apply <code>subst</code> to all id's in <code>instr</code>, including LHS id's</p></dd></dl><dl><dt class="spec value" id="val-hpred_sub"><a href="#val-hpred_sub" class="anchor"></a><code><span class="keyword">val</span> hpred_sub : <a href="index.html#type-subst">subst</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a></code></dt></dl></section><section><header><h3 id="functions-for-replacing-occurrences-of-expressions."><a href="#functions-for-replacing-occurrences-of-expressions." class="anchor"></a>Functions for replacing occurrences of expressions.</h3></header><dl><dt class="spec value" id="val-exp_replace_exp"><a href="#val-exp_replace_exp" class="anchor"></a><code><span class="keyword">val</span> exp_replace_exp : <span><span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a></code></dt><dt class="spec value" id="val-atom_replace_exp"><a href="#val-atom_replace_exp" class="anchor"></a><code><span class="keyword">val</span> atom_replace_exp : <span><span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a> <span>&#45;&gt;</span> <a href="index.html#type-atom">atom</a></code></dt><dt class="spec value" id="val-hpred_replace_exp"><a href="#val-hpred_replace_exp" class="anchor"></a><code><span class="keyword">val</span> hpred_replace_exp : <span><span>(<a href="../Exp/index.html#type-t">Exp.t</a> * <a href="../Exp/index.html#type-t">Exp.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a> <span>&#45;&gt;</span> <a href="index.html#type-hpred">hpred</a></code></dt></dl></section><section><header><h3 id="functions-for-constructing-or-destructing-entities-in-this-module"><a href="#functions-for-constructing-or-destructing-entities-in-this-module" class="anchor"></a>Functions for constructing or destructing entities in this module</h3></header><dl><dt class="spec value" id="val-exp_get_offsets"><a href="#val-exp_get_offsets" class="anchor"></a><code><span class="keyword">val</span> exp_get_offsets : <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-offset">offset</a> list</span></code></dt><dd><p>Compute the offset list of an expression</p></dd></dl><dl><dt class="spec value" id="val-exp_add_offsets"><a href="#val-exp_add_offsets" class="anchor"></a><code><span class="keyword">val</span> exp_add_offsets : <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-offset">offset</a> list</span> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a></code></dt><dd><p>Add the offset list to an expression</p></dd></dl><dl><dt class="spec value" id="val-sigma_to_sigma_ne"><a href="#val-sigma_to_sigma_ne" class="anchor"></a><code><span class="keyword">val</span> sigma_to_sigma_ne : <span><a href="index.html#type-hpred">hpred</a> list</span> <span>&#45;&gt;</span> <span><span>(<span><a href="index.html#type-atom">atom</a> list</span> * <span><a href="index.html#type-hpred">hpred</a> list</span>)</span> list</span></code></dt><dt class="spec value" id="val-hpara_instantiate"><a href="#val-hpara_instantiate" class="anchor"></a><code><span class="keyword">val</span> hpara_instantiate : <a href="index.html#type-hpara">hpara</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span> * <span><a href="index.html#type-hpred">hpred</a> list</span></code></dt><dd><p><code>hpara_instantiate para e1 e2 elist</code> instantiates <code>para</code> with <code>e1</code>, <code>e2</code> and <code>elist</code>. If <code>para = lambda (x, y, xs). exists zs. b</code>, then the result of the instantiation is <code>b[e1 / x, e2 / y, elist / xs, _zs'/ zs]</code> for some fresh <code>_zs'</code>.</p></dd></dl><dl><dt class="spec value" id="val-hpara_dll_instantiate"><a href="#val-hpara_dll_instantiate" class="anchor"></a><code><span class="keyword">val</span> hpara_dll_instantiate : <a href="index.html#type-hpara_dll">hpara_dll</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <a href="../Exp/index.html#type-t">Exp.t</a> <span>&#45;&gt;</span> <span><a href="../Exp/index.html#type-t">Exp.t</a> list</span> <span>&#45;&gt;</span> <span><a href="../Ident/index.html#type-t">Ident.t</a> list</span> * <span><a href="index.html#type-hpred">hpred</a> list</span></code></dt><dd><p><code>hpara_dll_instantiate para cell blink flink  elist</code> instantiates <code>para</code> with <code>cell</code>, <code>blink</code>, <code>flink</code>, and <code>elist</code>. If <code>para = lambda (x, y, z, xs). exists zs. b</code>, then the result of the instantiation is <code>b[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs]</code> for some fresh <code>_zs'</code>.</p></dd></dl><dl><dt class="spec value" id="val-custom_error"><a href="#val-custom_error" class="anchor"></a><code><span class="keyword">val</span> custom_error : <a href="../Pvar/index.html#type-t">Pvar.t</a></code></dt></dl></section></div></body></html>